Termination proof of /tmp/tmpKGJbBn/A04.itrs

Termination of the given ITRSProblem could successfully be proven:

↳ ITRS

  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

cond(y, x, y) → +@z(1@z, minus(x, +@z(y, 1@z)))
min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u
minus(x, x) → 0@z
minus(x, y) → cond(min(x, y), x, y)

The set Q consists of the following terms:

cond(x0, x1, x0)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

Added dependency pairs

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

cond(y, x, y) → +@z(1@z, minus(x, +@z(y, 1@z)))
min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u
minus(x, x) → 0@z
minus(x, y) → cond(min(x, y), x, y)

The integer pair graph contains the following rules and edges:

(0): MINUS(x[0], y[0]) → MIN(x[0], y[0])
(1): COND(y[1], x[1], y[1]) → MINUS(x[1], +@z(y[1], 1@z))
(2): MIN(u[2], v[2]) → IF(<@z(u[2], v[2]), u[2], v[2])
(3): MINUS(x[3], y[3]) → COND(min(x[3], y[3]), x[3], y[3])

(0) -> (2), if ((y[0] →^* v[2])∧(x[0] →^* u[2]))

(1) -> (0), if ((+@z(y[1], 1@z) →^* y[0])∧(x[1] →^* x[0]))

(1) -> (3), if ((+@z(y[1], 1@z) →^* y[3])∧(x[1] →^* x[3]))

(3) -> (1), if ((x[3] →^* x[1])∧(y[3] →^* y[1])∧(min(x[3], y[3]) →^* y[1]))

The set Q consists of the following terms:

cond(x0, x1, x0)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u

(0) -> (2), if ((y[0] →^* v[2])∧(x[0] →^* u[2]))

(1) -> (0), if ((+@z(y[1], 1@z) →^* y[0])∧(x[1] →^* x[0]))

(1) -> (3), if ((+@z(y[1], 1@z) →^* y[3])∧(x[1] →^* x[3]))

(3) -> (1), if ((x[3] →^* x[1])∧(y[3] →^* y[1])∧(min(x[3], y[3]) →^* y[1]))

The set Q consists of the following terms:

cond(x0, x1, x0)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u

The integer pair graph contains the following rules and edges:

(1): COND(y[1], x[1], y[1]) → MINUS(x[1], +@z(y[1], 1@z))
(3): MINUS(x[3], y[3]) → COND(min(x[3], y[3]), x[3], y[3])

(3) -> (1), if ((x[3] →^* x[1])∧(y[3] →^* y[1])∧(min(x[3], y[3]) →^* y[1]))

(1) -> (3), if ((+@z(y[1], 1@z) →^* y[3])∧(x[1] →^* x[3]))

The set Q consists of the following terms:

cond(x0, x1, x0)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND(y[1], x[1], y[1]) → MINUS(x[1], +@z(y[1], 1@z)) the following chains were created:

We consider the chain MINUS(x[3], y[3]) → COND(min(x[3], y[3]), x[3], y[3]), COND(y[1], x[1], y[1]) → MINUS(x[1], +@z(y[1], 1@z)), MINUS(x[3], y[3]) → COND(min(x[3], y[3]), x[3], y[3]) which results in the following constraint:
(1)    (x[3]=x[1]∧min(x[3], y[3])=y[1]∧x[1]=x[3]1∧y[3]=y[1]∧+@z(y[1], 1@z)=y[3]1 ⇒ COND(y[1], x[1], y[1])≥NonInfC∧COND(y[1], x[1], y[1])≥MINUS(x[1], +@z(y[1], 1@z))∧(U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥))

We simplified constraint (1) using rules (III), (IV), (VII), (REWRITING) which results in the following new constraint:
(2)    (<@z(x[3], y[3])=x0∧if(x0, x[3], y[3])=y[3] ⇒ COND(y[3], x[3], y[3])≥NonInfC∧COND(y[3], x[3], y[3])≥MINUS(x[3], +@z(y[3], 1@z))∧(U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on if(x0, x[3], y[3])=y[3] which results in the following new constraints:
(3)    (x1=x1∧<@z(x2, x1)=FALSE ⇒ COND(x1, x2, x1)≥NonInfC∧COND(x1, x2, x1)≥MINUS(x2, +@z(x1, 1@z))∧(U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥))

(4)    (x4=x3∧<@z(x4, x3)=TRUE ⇒ COND(x3, x4, x3)≥NonInfC∧COND(x3, x4, x3)≥MINUS(x4, +@z(x3, 1@z))∧(U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥))

We simplified constraint (3) using rule (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:
(5)    (<@z(x2, x1)=FALSE ⇒ COND(x1, x2, x1)≥NonInfC∧COND(x1, x2, x1)≥MINUS(x2, +@z(x1, 1@z))∧(U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥))

We simplified constraint (4) using rule (III) which results in the following new constraint:
(6)    (<@z(x3, x3)=TRUE ⇒ COND(x3, x3, x3)≥NonInfC∧COND(x3, x3, x3)≥MINUS(x3, +@z(x3, 1@z))∧(U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥))

We simplified constraint (5) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(7)    (x2 + (-1)x1 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x1 + x2 ≥ 0∧0 ≥ 0)

We simplified constraint (6) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    (-1 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound ≥ 0∧0 ≥ 0)

We simplified constraint (7) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    (x2 + (-1)x1 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x1 + x2 ≥ 0∧0 ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (-1 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound ≥ 0∧0 ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (x2 + (-1)x1 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x1 + x2 ≥ 0∧0 ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12)    (-1 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound ≥ 0∧0 ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(13)    (x1 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound + x1 ≥ 0∧0 ≥ 0)

We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(14)    (-1 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(15)    (x1 ≥ 0∧x2 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound + x1 ≥ 0∧0 ≥ 0)

(16)    (x1 ≥ 0∧x2 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound + x1 ≥ 0∧0 ≥ 0)

We solved constraint (14) using rule (IDP_SMT_SPLIT).

For Pair MINUS(x[3], y[3]) → COND(min(x[3], y[3]), x[3], y[3]) the following chains were created:

We consider the chain COND(y[1], x[1], y[1]) → MINUS(x[1], +@z(y[1], 1@z)), MINUS(x[3], y[3]) → COND(min(x[3], y[3]), x[3], y[3]), COND(y[1], x[1], y[1]) → MINUS(x[1], +@z(y[1], 1@z)) which results in the following constraint:
(17)    (x[3]=x[1]1∧min(x[3], y[3])=y[1]1∧x[1]=x[3]∧y[3]=y[1]1∧+@z(y[1], 1@z)=y[3] ⇒ MINUS(x[3], y[3])≥NonInfC∧MINUS(x[3], y[3])≥COND(min(x[3], y[3]), x[3], y[3])∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥))

We simplified constraint (17) using rules (III), (IV), (VII), (REWRITING) which results in the following new constraint:
(18)    (<@z(x[3], +@z(y[1], 1@z))=x5∧+@z(y[1], 1@z)=x6∧if(x5, x[3], x6)=+@z(y[1], 1@z) ⇒ MINUS(x[3], +@z(y[1], 1@z))≥NonInfC∧MINUS(x[3], +@z(y[1], 1@z))≥COND(min(x[3], +@z(y[1], 1@z)), x[3], +@z(y[1], 1@z))∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥))

We simplified constraint (18) using rule (V) (with possible (I) afterwards) using induction on if(x5, x[3], x6)=+@z(y[1], 1@z) which results in the following new constraints:
(19)    (x7=+@z(y[1], 1@z)∧<@z(x8, +@z(y[1], 1@z))=FALSE∧+@z(y[1], 1@z)=x7 ⇒ MINUS(x8, +@z(y[1], 1@z))≥NonInfC∧MINUS(x8, +@z(y[1], 1@z))≥COND(min(x8, +@z(y[1], 1@z)), x8, +@z(y[1], 1@z))∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥))

(20)    (x10=+@z(y[1], 1@z)∧<@z(x10, +@z(y[1], 1@z))=TRUE∧+@z(y[1], 1@z)=x9 ⇒ MINUS(x10, +@z(y[1], 1@z))≥NonInfC∧MINUS(x10, +@z(y[1], 1@z))≥COND(min(x10, +@z(y[1], 1@z)), x10, +@z(y[1], 1@z))∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥))

We simplified constraint (19) using rules (III), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:
(21)    (<@z(x8, +@z(y[1], 1@z))=FALSE ⇒ MINUS(x8, +@z(y[1], 1@z))≥NonInfC∧MINUS(x8, +@z(y[1], 1@z))≥COND(min(x8, +@z(y[1], 1@z)), x8, +@z(y[1], 1@z))∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥))

We simplified constraint (20) using rules (III), (IV) which results in the following new constraint:
(22)    (<@z(+@z(y[1], 1@z), +@z(y[1], 1@z))=TRUE ⇒ MINUS(+@z(y[1], 1@z), +@z(y[1], 1@z))≥NonInfC∧MINUS(+@z(y[1], 1@z), +@z(y[1], 1@z))≥COND(min(+@z(y[1], 1@z), +@z(y[1], 1@z)), +@z(y[1], 1@z), +@z(y[1], 1@z))∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥))

We simplified constraint (22) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(23)    (-1 ≥ 0 ⇒ (U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-1 + (-1)Bound ≥ 0∧0 ≥ 0)

We simplified constraint (21) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(24)    (-1 + x8 + (-1)y[1] ≥ 0 ⇒ (U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-2 + (-1)Bound + (-1)y[1] + x8 ≥ 0∧0 ≥ 0)

We simplified constraint (24) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(25)    (-1 + x8 + (-1)y[1] ≥ 0 ⇒ (U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-2 + (-1)Bound + (-1)y[1] + x8 ≥ 0∧0 ≥ 0)

We simplified constraint (23) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(26)    (-1 ≥ 0 ⇒ (U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-1 + (-1)Bound ≥ 0∧0 ≥ 0)

We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(27)    (-1 + x8 + (-1)y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-2 + (-1)Bound + (-1)y[1] + x8 ≥ 0)

We simplified constraint (26) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(28)    (-1 ≥ 0 ⇒ (U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-1 + (-1)Bound ≥ 0∧0 ≥ 0)

We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(29)    (y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-1 + (-1)Bound + y[1] ≥ 0)

We solved constraint (28) using rule (IDP_SMT_SPLIT).We simplified constraint (29) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(30)    (y[1] ≥ 0∧x8 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-1 + (-1)Bound + y[1] ≥ 0)

(31)    (y[1] ≥ 0∧x8 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-1 + (-1)Bound + y[1] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND(y[1], x[1], y[1]) → MINUS(x[1], +@z(y[1], 1@z))
- (x1 ≥ 0∧x2 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound + x1 ≥ 0∧0 ≥ 0)
- (x1 ≥ 0∧x2 ≥ 0 ⇒ (U^Increasing(MINUS(x[1], +@z(y[1], 1@z))), ≥)∧-1 + (-1)Bound + x1 ≥ 0∧0 ≥ 0)
MINUS(x[3], y[3]) → COND(min(x[3], y[3]), x[3], y[3])
- (y[1] ≥ 0∧x8 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-1 + (-1)Bound + y[1] ≥ 0)
- (y[1] ≥ 0∧x8 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(COND(min(x[3], y[3]), x[3], y[3])), ≥)∧-1 + (-1)Bound + y[1] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(if(x₁, x₂, x₃)) = -1 + (-1)x₃ + x₂ + (-1)x₁
POL(TRUE) = -1
POL(MINUS(x₁, x₂)) = -1 + (-1)x₂ + x₁
POL(+@z(x₁, x₂)) = x₁ + x₂
POL(FALSE) = -1
POL(COND(x₁, x₂, x₃)) = -1 + (-1)x₃ + x₂
POL(<@z(x₁, x₂)) = -1
POL(min(x₁, x₂)) = -1 + (-1)x₂ + (-1)x₁
POL(1@z) = 1
POL(undefined) = -1

The following pairs are in P_>:

COND(y[1], x[1], y[1]) → MINUS(x[1], +@z(y[1], 1@z))

The following pairs are in P_bound:

COND(y[1], x[1], y[1]) → MINUS(x[1], +@z(y[1], 1@z))
MINUS(x[3], y[3]) → COND(min(x[3], y[3]), x[3], y[3])

The following pairs are in P_≥:

MINUS(x[3], y[3]) → COND(min(x[3], y[3]), x[3], y[3])

At least the following rules have been oriented under context sensitive arithmetic replacement:

+@z¹ ↔

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

                ↳ AND

                  ↳ IDP

                    ↳ IDependencyGraphProof

                  ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u

The integer pair graph is empty.
The set Q consists of the following terms:

cond(x0, x1, x0)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

                ↳ AND

                  ↳ IDP

                  ↳ IDP

                    ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u

The integer pair graph contains the following rules and edges:

(3): MINUS(x[3], y[3]) → COND(min(x[3], y[3]), x[3], y[3])

The set Q consists of the following terms:

cond(x0, x1, x0)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.